(DEFPROP ALPHABETIC 
 (LAMBDA(R L)
  (PROG NIL
   A    (COND ((OR (NULL L) (NULL (CAR L))) (RETURN R))
	      ((NOT (EQ (LENGTH (CDR R)) (LENGTH (CDAR L)))) (GO B))
	      ((ALPHAV (CDR R) (CDAR L) NIL) (RETURN (CAR L))))
   B    (SETQ L (CDR L))
	(COND (L (GO A)) (T (RETURN NIL))))) 
EXPR)

(DEFPROP ALPHAV 
 (LAMBDA(C1 C2 L)
  (PROG NIL
   AL1  (COND ((NULL C1) (RETURN T)) ((NEG (CAR C1)) (GO AL3)) ((NOT (EQ (CAAR C1) (CAAR C2))) (RETURN NIL)))
	(SETQ L (ANSUNI (CDAR C1) (CDAR C2) L))
   AL2  (COND ((NULL L) (RETURN NIL)))
	(SETQ C1 (CDR C1))
	(SETQ C2 (CDR C2))
	(GO AL1)
   AL3  (COND ((POS (CAR C2)) (RETURN NIL))
	      ((EQ (CADAR C1) (CADAR C2)) (SETQ L (ANSUNI (CDDAR C1) (CDDAR C2) L)) (GO AL2)))
	(RETURN NIL))) 
EXPR)

(DEFPROP ANSPRED 
 (LAMBDA NIL (ANSPRINT (STAGE1 (ANSWER (CONS LHP RHP))))) 
EXPR)

(DEFPROP ANSPRINT 
 (LAMBDA(L)
  (PROG (Z VARL ONO)
	(SETQ ONO 0)
   B    (PRINC (QUOTE /())
	(SETQ Z (CDAR L))
   A    (COND ((NEG (CAR Z)) (PRFPR1 (CDAR Z))) (T (PRFPR1 (CONS ESCAPE (CAR Z)))))
	(SETQ Z (CDR Z))
	(COND (Z (PRINC (QUOTE / )) (PRINC (QUOTE ∧)) (PRINC (QUOTE / )) (GO A)))
	(PRINC (QUOTE /)))
	(SETQ L (CDR L))
	(COND (L (PRINC (QUOTE / )) (PRINC (QUOTE ∨)) (PRINC (QUOTE / )) (GO B)))
	(RETURN NIL))) 
EXPR)

(DEFPROP ANSWER 
 (LAMBDA(L)
  (PROG (SUBST TREE Z Z1 Z2 NO* NO1)
	(SETQ NO* NO)
	(SETQ NO1 NO)
	(SETQ Z (ANS1 L))
	(SETQ Z (REVERSE (SET3 (RESTORE1 (REVERSE (COPY Z))))))
	(SETQ Z1 Z)
   B    (SETQ Z2 (CAR Z1))
	(COND ((VINE Z2) (SETQ BL NIL) (STAND Z2)))
	(SETQ Z1 (CDR Z1))
	(COND (Z1 (GO B)))
	(SETQ TREE Z)
	(SETQ Z1 TREE)
	(SETQ NO 0)
	(SETQ SUBST (LIST NIL))
   C    (COND ((VINE (CAR TREE)) (GO D)))
	(SETQ Z (ANCESTOR (CAR TREE)))
	(SETQ Z (RES (CAR Z) (CDR Z) (CAR TREE)))
	(STAND1 (CAR TREE) (CDR Z))
	(ST2 (CAR Z) SUBST)
   D    (SETQ TREE (CDR TREE))
	(COND (TREE (GO C)))
	(SETQ NO NO1)
	(RETURN (NEGTHM Z1 (CDR SUBST))))) 
EXPR)

(DEFPROP ANSWER 
 (NIL ALPHABETIC
      ALPHAV
      ANSPRED
      ANSPRINT
      ANSWER
      IN
      NEGTHM
      SUBS
      ANSUNI
      ANS1
      COLLECT
      RES
      RES1
      STAGE1
      STAND
      STAND1
      ST2) 
VALUE)

(DEFPROP IN 
 (LAMBDA(T1 S)
  (PROG (Z)
   A    (COND ((NULL S) (RETURN NIL)))
	(SETQ Z (CAR S))
	(COND ((EQUAL (CDR Z) T1) (RETURN (CAR Z))))
	(SETQ S (CDR S))
	(GO A))) 
EXPR)

(DEFPROP NEGTHM 
 (LAMBDA(L S)
  (PROG (Z)
	(COND ((NULL L) (RETURN (LIST NIL))))
   A1   (COND ((NULL L) (RETURN Z))
	      ((AND (NUMBERP (CAR (ANCESTOR (CAR L)))) (MINUSP (CAR (ANCESTOR (CAR L)))))
	       (SETQ Z (CONS (SUBS S (CAR L)) Z))))
	(SETQ L (CDR L))
	(GO A1))) 
EXPR)

(DEFPROP SUBS 
 (LAMBDA(S C)
  (PROG (Z) (SETQ Z C) A (SETQ C (CDR C)) (COND ((NULL C) (RETURN Z))) (RPLACA C (SUBS3T S (CAR C))) (GO A))) 
EXPR)

(DEFPROP ANSUNI 
 (LAMBDA(C D L)
  (PROG (Z1 Z2 Z3)
   UN2  (SETQ Z2 (CAR D))
	(SETQ Z1 (SETQ Z3 (CAR C)))
	(COND
	 ((AND (VAR Z2) (VAR Z1)) (SETQ Z3 (SEARCH1 Z1 L))
				  (COND ((NULL Z3) (SETQ L (CONS (CONS Z1 Z2) L)) (GO UN1))
					((VAR Z3) (COND ((EQ Z3 Z2) (GO UN1)) (T (RETURN NIL)))))))
	(COND ((OR (VAR Z1) (VAR Z2)) (RETURN NIL))
	      ((CONST Z2) (COND ((EQ (CAR Z2) (CAR Z3)) (GO UN1)) (T (RETURN NIL))))
	      ((EQ (CAR Z2) (CAR Z3)) (SETQ C (APPEND (CDR Z3) (CDR C)))
				      (SETQ D (APPEND (CDR Z2) (CDR D)))
				      (GO UN2))
	      (T (RETURN NIL)))
   UN1  (SETQ C (CDR C))
	(COND (C (SETQ D (CDR D)) (GO UN2)))
	(COND (L (RETURN L)) (T (RETURN (LIST (CONS 64 64))))))) 
EXPR)

(DEFPROP ANS1 
 (LAMBDA(L)
  (PROG (Z Z2 Z3 Z4 Z5 L1 N)
	(SETQ N 1)
	(SETQ L (LIST (CONS (CONS NIL (CONS NIL (CONS 0 L))) (QUOTE ((ANS (A)))))))
   B    (SETQ Z2 (CAAR L))
	(SETQ Z3 (LENGTH (CDAR L)))
	(COND ((NULL (CADR Z2)) (SETQ Z4 NIL))
	      (T
	       (SETQ Z4
		     (PROG (Z Z1 N)
			   (SETQ N 0)
			   (SETQ Z1 (CDAR L))
			   (SETQ Z (CADR Z2))
 		      A    (COND ((EQ Z Z1) (RETURN N)))
			   (SETQ Z1 (CDR Z1))
			   (SETQ N (ADD1 N))
			   (GO A)))))
	(SETQ Z (CDDDR Z2))
	(COND ((NUMBERP (CDR Z))
	       (COND ((NOT (NUMBERP (CAR Z))) (RPLACD (LAST L) (LIST (CAAR Z) (CDAR Z)))
					      (SETQ Z5 (CONS N (ADD1 N)))
					      (SETQ N (ADD1 (ADD1 N))))
		     (T (SETQ Z5 (LIST Z)))))
	      (T (RPLACD (LAST L) (LIST (CAR Z) (CDR Z)))
		 (SETQ Z5 (CONS N (ADD1 N)))
		 (SETQ N (ADD1 (ADD1 N)))))
	(SETQ Z (CONS Z3 (CONS Z4 (CONS 0 Z5))))
	(SETQ L1 (CONS (CONS Z (CDAR L)) L1))
	(SETQ L (CDR L))
	(COND (L (GO B)))
	(RETURN L1))) 
EXPR)

(DEFPROP COLLECT 
 (LAMBDA(L S)
  (PROG (Z)
   A    (COND ((NULL L) (RETURN S))
	      ((VAR (CAR L)) NIL)
	      ((SETQ Z (IN (CAR L) S)) (RPLACA L Z))
	      ((MEMBER (CAAR L) THMLIST)
	       (RPLACA L (CAAR (SETQ S (CONS (CONS (SETQ NEWV (SUB1 NEWV)) (CAR L)) S)))))
	      (T (SETQ S (COLLECT (CDAR L) S))))
	(SETQ L (CDR L))
	(GO A))) 
EXPR)

(DEFPROP RES 
 (LAMBDA(C D R)
  (COND ((OR (ALLNEG D) (ALLPOS C)) (RES1 C D R))
	((OR (ALLPOS D) (ALLNEG C)) (RES1 D C R))
	(T (NCONC (RES1 C D R) (RES1 D C R))))) 
EXPR)

(DEFPROP RES1 
 (LAMBDA(C D R)
  (PROG (CB DB DB1 YC YD YD1 Z X Y RES)
	(COND ((EQ C D) (RETURN NIL)))
	(SETQ YC (CDR C))
	(SETQ CB (POSBIT C))
	(SETQ YD1 (NEGL D))
	(SETQ DB1 (NEGBIT D))
	(SETQ DB DB1)
	(SETQ YD YD1)
   RES1 (SETQ X (CAR YC))
	(COND ((NEG X) (RETURN NIL)))
	(SETQ Y (CAR YD))
	(COND ((ORDERP (CAR X) (CADR Y)) (GO RES3)) ((NOT (EQ (CAR X) (CADR Y))) (GO RES4)))
	(SETQ YD1 YD)
	(SETQ DB1 DB)
	(GO RES2A)
   RES2 (SETQ Y (CAR YD))
	(COND ((NOT (EQ (CAR X) (CADR Y))) (GO RES3A)))
   RES2A
	(COND ((NOT (UNIFAB (CAR CB) (CAR DB))) (GO RES2B)))
	(SETQ Z (UNIFY (CDR X) (CDDR Y)))
	(COND
	 (Z (SETQ PARRES NIL)
	    (COND ((SETQ RES (ALPHABETIC R (UNION (CDR Z) C D X Y))) (RETURN (CONS (CDR Z) RES))) (T NIL))))
   RES2B
	(SETQ YD (CDR YD))
	(SETQ DB (CDR DB))
	(COND (YD (GO RES2)))
   RES3A
	(SETQ DB DB1)
	(SETQ YD YD1)
   RES3 (SETQ YC (CDR YC))
	(SETQ CB (CDR CB))
	(COND (YC (GO RES1)))
	(RETURN NIL)
   RES4 (SETQ YD (CDR YD))
	(SETQ DB (CDR DB))
	(COND (YD (GO RES1)))
	(GO RES3A))) 
EXPR)

(DEFPROP STAGE1 
 (LAMBDA(L)
  (PROG (Z Z1 S NEWV)
	(SETQ Z L)
	(SETQ NEWV -1)
   B    (SETQ Z1 (CDAR Z))
   A    (COND ((NEG (CAR Z1)) (SETQ S (COLLECT (CDDAR Z1) S))) (T (SETQ S (COLLECT (CDAR Z1) S))))
	(SETQ Z1 (CDR Z1))
	(COND (Z1 (GO A)))
	(SETQ Z (CDR Z))
	(COND (Z (GO B)))
	(RETURN L))) 
EXPR)

(DEFPROP STAND 
 (LAMBDA (X) (PROG (Z) (SETQ Z (CDR X)) A (UPIT (CAR Z)) (SETQ Z (CDR Z)) (COND (Z (GO A))) (RETURN X))) 
EXPR)

(DEFPROP STAND1 
 (LAMBDA(OL NE)
  (PROG (Z Z1)
	(RPLACA (CAAR OL) (CAAR NE))
	(SETQ Z (CDR OL))
	(SETQ Z1 (CDR NE))
   A    (RPLACA Z (CAR Z1))
	(SETQ Z (CDR Z))
	(SETQ Z1 (CDR Z1))
	(COND (Z (GO A)))
	(RETURN NIL))) 
EXPR)

(DEFPROP ST2 
 (LAMBDA(L1 L)
  (PROG (L2) A (COND ((NULL L1) (RETURN NIL))) (SUBS2T (CDAR L1) (CAAR L1) L) (SETQ L1 (CDR L1)) (GO A))) 
EXPR)


(DEFPROP REENTER 
 (LAMBDA NIL (PROG NIL (ATTEMPT1 XYZ2) (RETURN NIL))) 
EXPR)

(DEFPROP RESTORE 
 (LAMBDA(IL)
  (PROG (ZZ) (EVAL (CONS (QUOTE INPUT) IL)) (INC T) (SETQ ZZ (RESTORE1 (READ))) (INC NIL) (RETURN (SET3 ZZ)))) 
FEXPR)